Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/monoid_algebra): add mem.span_support #7323

Closed
wants to merge 4 commits into from

Conversation

riccardobrasca
Copy link
Member

A (very) easy lemma about monoid_algebra.


Open in Gitpod

@riccardobrasca riccardobrasca added the awaiting-review The author would like community review of the PR label Apr 22, 2021
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

I've added comments only for the multiplicative version, but they apply to the additive version too.

@bors
Copy link

bors bot commented Apr 22, 2021

✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

riccardobrasca and others added 3 commits April 22, 2021 15:15
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@riccardobrasca
Copy link
Member Author

bors r+

bors bot pushed a commit that referenced this pull request Apr 22, 2021
A (very) easy lemma about `monoid_algebra`.
@eric-wieser eric-wieser added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 22, 2021
@bors
Copy link

bors bot commented Apr 22, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/monoid_algebra): add mem.span_support [Merged by Bors] - feat(algebra/monoid_algebra): add mem.span_support Apr 22, 2021
@bors bors bot closed this Apr 22, 2021
@bors bors bot deleted the monoid_alg_lemmas branch April 22, 2021 20:21
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants